0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 89 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 105 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 0 ms)
↳23 QDP
↳24 Rewriting (⇔, 0 ms)
↳25 QDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 QDP
↳28 QReductionProof (⇔, 0 ms)
↳29 QDP
↳30 Rewriting (⇔, 0 ms)
↳31 QDP
↳32 UsableRulesProof (⇔, 0 ms)
↳33 QDP
↳34 QReductionProof (⇔, 0 ms)
↳35 QDP
↳36 Instantiation (⇔, 0 ms)
↳37 QDP
↳38 QDPOrderProof (⇔, 84 ms)
↳39 QDP
↳40 DependencyGraphProof (⇔, 0 ms)
↳41 TRUE
PERMB_IN_GA(.(X1, X2), .(X3, X4)) → U3_GA(X1, X2, X3, X4, app1A_in_aaag(X5, X3, X6, X2))
PERMB_IN_GA(.(X1, X2), .(X3, X4)) → APP1A_IN_AAAG(X5, X3, X6, X2)
APP1A_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → U1_AAAG(X1, X2, X3, X4, X5, app1A_in_aaag(X2, X3, X4, X5))
APP1A_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APP1A_IN_AAAG(X2, X3, X4, X5)
PERMB_IN_GA(.(X1, X2), .(X3, X4)) → U4_GA(X1, X2, X3, X4, app1cA_in_aaag(X5, X3, X6, X2))
U4_GA(X1, X2, X3, X4, app1cA_out_aaag(X5, X3, X6, X2)) → U5_GA(X1, X2, X3, X4, app2E_in_gga(X5, X6, X7))
U4_GA(X1, X2, X3, X4, app1cA_out_aaag(X5, X3, X6, X2)) → APP2E_IN_GGA(X5, X6, X7)
APP2E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U2_GGA(X1, X2, X3, X4, app2E_in_gga(X2, X3, X4))
APP2E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APP2E_IN_GGA(X2, X3, X4)
U4_GA(X1, X2, X3, X4, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, X3, X4, app2cC_in_ggga(X1, X5, X6, X7))
U6_GA(X1, X2, X3, X4, app2cC_out_ggga(X1, X5, X6, X7)) → U7_GA(X1, X2, X3, X4, permB_in_ga(X7, X4))
U6_GA(X1, X2, X3, X4, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7, X4)
PERMB_IN_GA(.(X1, X2), .(X1, X3)) → U8_GA(X1, X2, X3, app2cD_in_ga(X2, X4))
U8_GA(X1, X2, X3, app2cD_out_ga(X2, X4)) → U9_GA(X1, X2, X3, permB_in_ga(X4, X3))
U8_GA(X1, X2, X3, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4, X3)
app1cA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, app1cA_in_aaag(X2, X3, X4, X5))
app1cA_in_aaag([], X1, X2, .(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X2, X3, X4, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app2cC_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga([], X1, X1) → app2cE_out_gga([], X1, X1)
U17_gga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
app2cD_in_ga(X1, X1) → app2cD_out_ga(X1, X1)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
PERMB_IN_GA(.(X1, X2), .(X3, X4)) → U3_GA(X1, X2, X3, X4, app1A_in_aaag(X5, X3, X6, X2))
PERMB_IN_GA(.(X1, X2), .(X3, X4)) → APP1A_IN_AAAG(X5, X3, X6, X2)
APP1A_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → U1_AAAG(X1, X2, X3, X4, X5, app1A_in_aaag(X2, X3, X4, X5))
APP1A_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APP1A_IN_AAAG(X2, X3, X4, X5)
PERMB_IN_GA(.(X1, X2), .(X3, X4)) → U4_GA(X1, X2, X3, X4, app1cA_in_aaag(X5, X3, X6, X2))
U4_GA(X1, X2, X3, X4, app1cA_out_aaag(X5, X3, X6, X2)) → U5_GA(X1, X2, X3, X4, app2E_in_gga(X5, X6, X7))
U4_GA(X1, X2, X3, X4, app1cA_out_aaag(X5, X3, X6, X2)) → APP2E_IN_GGA(X5, X6, X7)
APP2E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U2_GGA(X1, X2, X3, X4, app2E_in_gga(X2, X3, X4))
APP2E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APP2E_IN_GGA(X2, X3, X4)
U4_GA(X1, X2, X3, X4, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, X3, X4, app2cC_in_ggga(X1, X5, X6, X7))
U6_GA(X1, X2, X3, X4, app2cC_out_ggga(X1, X5, X6, X7)) → U7_GA(X1, X2, X3, X4, permB_in_ga(X7, X4))
U6_GA(X1, X2, X3, X4, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7, X4)
PERMB_IN_GA(.(X1, X2), .(X1, X3)) → U8_GA(X1, X2, X3, app2cD_in_ga(X2, X4))
U8_GA(X1, X2, X3, app2cD_out_ga(X2, X4)) → U9_GA(X1, X2, X3, permB_in_ga(X4, X3))
U8_GA(X1, X2, X3, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4, X3)
app1cA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, app1cA_in_aaag(X2, X3, X4, X5))
app1cA_in_aaag([], X1, X2, .(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X2, X3, X4, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app2cC_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga([], X1, X1) → app2cE_out_gga([], X1, X1)
U17_gga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
app2cD_in_ga(X1, X1) → app2cD_out_ga(X1, X1)
APP2E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APP2E_IN_GGA(X2, X3, X4)
app1cA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, app1cA_in_aaag(X2, X3, X4, X5))
app1cA_in_aaag([], X1, X2, .(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X2, X3, X4, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app2cC_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga([], X1, X1) → app2cE_out_gga([], X1, X1)
U17_gga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
app2cD_in_ga(X1, X1) → app2cD_out_ga(X1, X1)
APP2E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APP2E_IN_GGA(X2, X3, X4)
APP2E_IN_GGA(.(X1, X2), X3) → APP2E_IN_GGA(X2, X3)
From the DPs we obtained the following set of size-change graphs:
APP1A_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APP1A_IN_AAAG(X2, X3, X4, X5)
app1cA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, app1cA_in_aaag(X2, X3, X4, X5))
app1cA_in_aaag([], X1, X2, .(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X2, X3, X4, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app2cC_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga([], X1, X1) → app2cE_out_gga([], X1, X1)
U17_gga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
app2cD_in_ga(X1, X1) → app2cD_out_ga(X1, X1)
APP1A_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APP1A_IN_AAAG(X2, X3, X4, X5)
APP1A_IN_AAAG(.(X1, X5)) → APP1A_IN_AAAG(X5)
From the DPs we obtained the following set of size-change graphs:
PERMB_IN_GA(.(X1, X2), .(X3, X4)) → U4_GA(X1, X2, X3, X4, app1cA_in_aaag(X5, X3, X6, X2))
U4_GA(X1, X2, X3, X4, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, X3, X4, app2cC_in_ggga(X1, X5, X6, X7))
U6_GA(X1, X2, X3, X4, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7, X4)
PERMB_IN_GA(.(X1, X2), .(X1, X3)) → U8_GA(X1, X2, X3, app2cD_in_ga(X2, X4))
U8_GA(X1, X2, X3, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4, X3)
app1cA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, app1cA_in_aaag(X2, X3, X4, X5))
app1cA_in_aaag([], X1, X2, .(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X2, X3, X4, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app2cC_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, app2cE_in_gga(X2, X3, X4))
app2cE_in_gga([], X1, X1) → app2cE_out_gga([], X1, X1)
U17_gga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
app2cD_in_ga(X1, X1) → app2cD_out_ga(X1, X1)
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, app2cC_in_ggga(X1, X5, X6))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_in_ga(X2))
U8_GA(X1, X2, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4)
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app2cC_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
app2cD_in_ga(X1) → app2cD_out_ga(X1, X1)
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cC_in_ggga(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
app2cD_in_ga(x0)
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_in_ga(X2))
U8_GA(X1, X2, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4)
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app2cC_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
app2cD_in_ga(X1) → app2cD_out_ga(X1, X1)
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cC_in_ggga(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
app2cD_in_ga(x0)
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_in_ga(X2))
U8_GA(X1, X2, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4)
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
app2cD_in_ga(X1) → app2cD_out_ga(X1, X1)
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cC_in_ggga(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
app2cD_in_ga(x0)
app2cC_in_ggga(x0, x1, x2)
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_in_ga(X2))
U8_GA(X1, X2, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4)
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
app2cD_in_ga(X1) → app2cD_out_ga(X1, X1)
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
app2cD_in_ga(x0)
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_out_ga(X2, X2))
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
U8_GA(X1, X2, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4)
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_out_ga(X2, X2))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
app2cD_in_ga(X1) → app2cD_out_ga(X1, X1)
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
app2cD_in_ga(x0)
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
U8_GA(X1, X2, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4)
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_out_ga(X2, X2))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
app2cD_in_ga(x0)
app2cD_in_ga(x0)
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
U8_GA(X1, X2, app2cD_out_ga(X2, X4)) → PERMB_IN_GA(X4)
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_out_ga(X2, X2))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U8_GA(z0, z1, app2cD_out_ga(z1, z1)) → PERMB_IN_GA(z1)
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_out_ga(X2, X2))
U8_GA(z0, z1, app2cD_out_ga(z1, z1)) → PERMB_IN_GA(z1)
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U4_GA(X1, X2, app1cA_out_aaag(X5, X3, X6, X2)) → U6_GA(X1, X2, U18_ggga(X1, X5, X6, app2cE_in_gga(X5, X6)))
U8_GA(z0, z1, app2cD_out_ga(z1, z1)) → PERMB_IN_GA(z1)
POL(.(x1, x2)) = 1 + x2
POL(PERMB_IN_GA(x1)) = x1
POL(U11_aaag(x1, x2, x3)) = 1 + x3
POL(U17_gga(x1, x2, x3, x4)) = 1 + x4
POL(U18_ggga(x1, x2, x3, x4)) = x4
POL(U4_GA(x1, x2, x3)) = 1 + x3
POL(U6_GA(x1, x2, x3)) = x3
POL(U8_GA(x1, x2, x3)) = 1 + x2
POL([]) = 0
POL(app1cA_in_aaag(x1)) = x1
POL(app1cA_out_aaag(x1, x2, x3, x4)) = 1 + x1 + x3
POL(app2cC_out_ggga(x1, x2, x3, x4)) = x4
POL(app2cD_out_ga(x1, x2)) = 0
POL(app2cE_in_gga(x1, x2)) = 1 + x1 + x2
POL(app2cE_out_gga(x1, x2, x3)) = 1 + x3
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
PERMB_IN_GA(.(X1, X2)) → U4_GA(X1, X2, app1cA_in_aaag(X2))
U6_GA(X1, X2, app2cC_out_ggga(X1, X5, X6, X7)) → PERMB_IN_GA(X7)
PERMB_IN_GA(.(X1, X2)) → U8_GA(X1, X2, app2cD_out_ga(X2, X2))
app2cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, app2cE_in_gga(X2, X3))
app2cE_in_gga([], X1) → app2cE_out_gga([], X1, X1)
U18_ggga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cC_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, app2cE_out_gga(X2, X3, X4)) → app2cE_out_gga(.(X1, X2), X3, .(X1, X4))
app1cA_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, app1cA_in_aaag(X5))
app1cA_in_aaag(.(X1, X2)) → app1cA_out_aaag([], X1, X2, .(X1, X2))
U11_aaag(X1, X5, app1cA_out_aaag(X2, X3, X4, X5)) → app1cA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
app1cA_in_aaag(x0)
U11_aaag(x0, x1, x2)
app2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)